(set-logic LIA)
(synth-fun findSum ( (y1 Int) (y2 Int) (y3 Int) (y4 Int) (y5 Int) (y6 Int) (y7 Int) (y8 Int) (y9 Int) (y10 Int) )Int ((Start Int ( 0 1 2 3 4 5 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 z (+ Start Start)  (let ((z Int Start)) Start)  (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start)))))
(declare-var x1 Int)
(declare-var x2 Int)
(declare-var x3 Int)
(declare-var x4 Int)
(declare-var x5 Int)
(declare-var x6 Int)
(declare-var x7 Int)
(declare-var x8 Int)
(declare-var x9 Int)
(declare-var x10 Int)
(constraint (=> (> (+ x1 x2) 5) (= (findSum x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ) (+ x1 x2))))
(constraint (=> (and (<= (+ x1 x2) 5) (> (+ x2 x3) 5)) (= (findSum x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ) (+ x2 x3))))
(constraint (=> (and (and (<= (+ x1 x2) 5) (<= (+ x2 x3) 5)) (> (+ x3 x4) 5)) (= (findSum x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ) (+ x3 x4))))
(constraint (=> (and (and (<= (+ x1 x2) 5) (and (<= (+ x2 x3) 5) (<= (+ x3 x4) 5))) (> (+ x4 x5) 5)) (= (findSum x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ) (+ x4 x5))))
(constraint (=> (and (and (<= (+ x1 x2) 5) (and (<= (+ x2 x3) 5) (and (<= (+ x3 x4) 5) (<= (+ x4 x5) 5)))) (> (+ x5 x6) 5)) (= (findSum x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ) (+ x5 x6))))
(constraint (=> (and (and (<= (+ x1 x2) 5) (and (<= (+ x2 x3) 5) (and (<= (+ x3 x4) 5) (and (<= (+ x4 x5) 5) (<= (+ x5 x6) 5))))) (> (+ x6 x7) 5)) (= (findSum x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ) (+ x6 x7))))
(constraint (=> (and (and (<= (+ x1 x2) 5) (and (<= (+ x2 x3) 5) (and (<= (+ x3 x4) 5) (and (<= (+ x4 x5) 5) (and (<= (+ x5 x6) 5) (<= (+ x6 x7) 5)))))) (> (+ x7 x8) 5)) (= (findSum x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ) (+ x7 x8))))
(constraint (=> (and (and (<= (+ x1 x2) 5) (and (<= (+ x2 x3) 5) (and (<= (+ x3 x4) 5) (and (<= (+ x4 x5) 5) (and (<= (+ x5 x6) 5) (and (<= (+ x6 x7) 5) (<= (+ x7 x8) 5))))))) (> (+ x8 x9) 5)) (= (findSum x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ) (+ x8 x9))))
(constraint (=> (and (and (<= (+ x1 x2) 5) (and (<= (+ x2 x3) 5) (and (<= (+ x3 x4) 5) (and (<= (+ x4 x5) 5) (and (<= (+ x5 x6) 5) (and (<= (+ x6 x7) 5) (and (<= (+ x7 x8) 5) (<= (+ x8 x9) 5)))))))) (> (+ x9 x10) 5)) (= (findSum x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ) (+ x9 x10))))
(constraint (=> (and (<= (+ x1 x2) 5) (and (<= (+ x2 x3) 5) (and (<= (+ x3 x4) 5) (and (<= (+ x4 x5) 5) (and (<= (+ x5 x6) 5) (and (<= (+ x6 x7) 5) (and (<= (+ x7 x8) 5) (and (<= (+ x8 x9) 5) (<= (+ x9 x10) 5))))))))) (= (findSum x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ) 0)))
(check-synth)
(define-fun res ((Param0 Int) (Param1 Int) (Param2 Int) (Param3 Int) (Param4 Int) (Param5 Int) (Param6 Int) (Param7 Int) (Param8 Int) (Param9 Int)) Int (ite (< 5 (+ Param0 Param1)) (+ Param0 Param1) (ite (< 5 (+ Param1 Param2)) (+ Param1 Param2) (ite (< 5 (+ Param2 Param3)) (+ Param2 Param3) (ite (< 5 (+ Param3 Param4)) (+ Param3 Param4) (ite (< 5 (+ Param4 Param5)) (+ Param4 Param5) (ite (< 5 (+ Param5 Param6)) (+ Param5 Param6) (ite (< 5 (+ Param6 Param7)) (+ Param6 Param7) (ite (< 5 (+ Param7 Param8)) (+ Param7 Param8) (ite (< 5 (+ Param8 Param9)) (+ Param8 Param9) 0))))))))))